Nuprl Lemma : EVal_to_ES_wf 0,22
e:EventsWithValues, p:AtomFreeDecls(e). EVal_to_ES{i:l}(e,p)  ES0 
latex

DefinitionsEventsWithValues, t  T, x:A. B(x), AtomFreeDecls(X), ES0, x:AB(x), P  Q, EVal-to-ES, f(a), EVal_to_ES{i:l}(e,p)
LemmasEVal-to-ES, event-system0 wf, EVal-atom-free wf, EVal wf

origin